$\forall$$T$:Type, $L$:$T$ List, $P$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow\mathbb{B}$), ${\it T'}$:Type, $f$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \& $P$($x$) \}$\rightarrow$${\it T'}$), $x$:${\it T'}$.
\\[0ex]($x$ $\in$ mapfilter($f$;$P$;$L$)) $\Leftrightarrow$ ($\exists$$y$:$T$. ($y$ $\in$ $L$) \& $P$($y$) \& $x$ $=$ $f$($y$))